Model Driven Development (MDD) has been increasingly used in the last decade for
software development and, in many cases, has replaced traditional, code-centric
approaches.
In MDD, \emph{models} or software abstractions are the basic building blocks in
the software development life cycle and \emph{model transformations} are the
technology used to map between models conforming to different metamodels.
Transformations are used for different purposes in MDD, e.g., refactoring,
migration, and code generation.
Since transformations are essential in MDD, transformation testing
and verification is essential to the success of MDD.

Several studies have reported on industrial experiences in adopting
MDD~\cite{a15,indusREV}.
%% INDUSREV REVIEWS A FEW OF THEM, WE CAN REMOVE THE
% SENCOND REF IF WE DONT HAVE SPACE 4 IT
However, only a few of them have specifically discussed using model
transformations in industry. Daghsen \emph{et al.}~\cite{daghsen2010applying}
used transformations to map AUTOSAR timing models to classical scheduling models to
perform timing analysis. Giese \emph{et al.}~\cite{giese2010model} used triple
graph grammars to synchronize SysML system engineering models with AUTOSAR software
engineering models. Studies reporting on automated verification of industrial
transformations have also been limited.
%Use of MDD/model transformations/verif in industry

In this study, we report on using a light-weight, automated verification
prototype to reason about the correctness of an ATL~\cite{Jouault2008ATL}
transformation developed for the automotive industry~\cite{ECMFApaper}. More
specifically, we check the correctness of the transformation with respect to OCL
well-formedness constraints after translating the ATL transformation into a
logical satisfiability problem.  The basic approach has been presented in
previous work~\cite{Buettner2012ICFEM} but to our knowledge we are the first
reporting on its application to an industrial-sized verification problem.

While the transformation itself is not exceptionally large (in the number of
transformation rules), the corresponding metamodels are. Together, they comprise
1586 classes, 897 associations, and 371 multiplicity constraints. Since even
types not directly touched by the transformation are relevant for the
verification (due to constraints that relate them), we have to deal with 
large potential instances. To verify our transformation, we have successfully
checked \begin{changebar}models of up to $20000$ potential elements\end{changebar} with reasonable
runtimes (although all counter examples found contained much fewer elements and were found quite quickly). Hence we claim that the verification approach is applicable to
realistic verification scenarios.
% First, we revisit a transformation we developed for General Motors to migrate GM
% legacy models to their equivalent AUTOSAR models. 
% We describe
% an automated transformation verification prototype, and we demonstrate how the
% prototype can be used to verify our transformation, the results achieved, and
% the lessons learned.

The rest of this paper is organized as follows:
Section~\ref{sec:MT_AutomotiveIndustry} gives an overview of the GM-to-AUTOSAR
transformation previously presented in~\cite{ECMFApaper}; Section
\ref{sec:FormalVer_ConstSolvers} introduces the applied verification approach
and prototype; Section ~\ref{sec:caseStudy} describes the case study conducted
to verify the GM-to-AUTOSAR transformation using the aforementioned prototype;
Section~\ref{sec:results} summarizes the results of the case study and
investigates the performance of the used approach; Section~\ref{sec:discussion}
discusses its strengths and limitations; Section~\ref{sec:RelatedWork}
summarizes related work in the literature and Section~\ref{sec:concFW}
concludes and discusses future work.
